a, b:, E, F:({a..b}).
(j:. (a  j)  (j < b)  E(j)  F(j))  a  j < b. E(j)  a  j < b. F(j) 

latex

Definitions

ff, tt, if b then t else f fi , Y, t.2, t.1, 0, +r, e, *, (op,id) lb  i < ub. E(i), r+gp,  lb  i < ub. E(i), <+*>, (r) i  k < j. E(k), a  j < b. E(j), suptype(S; T), S  T, False, A, A  B, True, T, P  Q, P  Q, P & Q, i  j < k, x. t(x), t  T, {T}, , x(s), {i..j}, P  Q, x:A. B(x), Unit, , P  Q, Dec(P), {i...},

Lemmas

assert of le int, bnot of lt int, eqff to assert, assert of lt int, eqtt to assert, iff transitivity, bnot wf, le int wf, assert wf, bool wf, lt int wf, decidable le, qadd wf, qle transitivity qorder, qadd com, grp op preserves le qorder, sum unroll hi q, int-rational, qle weakening eq qorder, sum unroll base q, true wf, squash wf, int upper ind, int upper wf, qsum wf, qle wf, le wf, rationals wf, int seg wf, int le to int upper